import os
import simsym
import symtypes
import errno
import model
import signal
import ptypes
import PROCPRIOQUEUE
import Lock
import Context
import ProcessTable

PRIO = simsym.SInt;

class CURRENTPROCESS(simsym.tstruct(
		currentp = ptypes.PREF,
		readyqp = PROCPRIOQUEUE.PROCPRIOQUEUE,
		ctxt = Context.Context,
		lck = Lock.Lock
		#ptab = ProcessTable.ProcessTable
                )):
	def _declare_assumptions(self, assume):
		super(CURRENTPROCESS, self)._declare_assumptions(assume)
	
	@model.methodwrap(ct = Context.Context, lk = Lock.Lock)
	def INIT(self, ct, lk):
		self.readyqp.INIT
		self.currentp = ptypes.NullProcRef
		self.ctxt = ct
		self.lck = lk
	
	@model.methodwrap()
	def CurrentProcess(self):
		return self.currentp

	@model.methodwrap(pid = ptypes.PREF)
	def MakeCurrent(self, pid):
		self.currentp = pid

	@model.methodwrap(pid = ptypes.IPREF)
	def MakeReady(self, pid):
		#pd = ctxt.ptab.DescrOfProcess(pid)
		#prio = pd.ProcessPriority
		return True

	@model.methodwrap(pid = ptypes.PREF)
	def MakeUnready(self, pid):
		self.lck.Lock
		if self.isCurrentProc(pid):
			self.ctxt.SaveState
			self.RunNextProcess
		self.lck.Unlock

	@model.methodwrap(p = ptypes.PREF)
	def isCurrentProc(self, p):
		return self.currentp == p

	@model.methodwrap(
		currentp = ptypes.PREF,
		readyqp = PROCPRIOQUEUE.PROCPRIOQUEUE)
	def reloadCurrent(self, currentp, readyqp):
		self.currentp = currentp
		self.readyqp = readyqp

	@model.methodwrap(
		currentp = ptypes.PREF,
		readyqp = PROCPRIOQUEUE.PROCPRIOQUEUE)
	def ContinueCurrent(self, currentp, readyqp):
		self.reloadCurrent(currentp, readyqp)
		self.ctxt.RestoreState

	@model.methodwrap()
	def SuspendCurrent(self):
		self.lck.Lock
		self.ctxt.SaveState
		#pd = ctxt.ptab.DescrOfProcess(currentp)
		self.lck.Unlock

	@model.methodwrap()
	def RunNextProcess(self):
		self.SCHEDULENEXT
		self.ctxt.RestoreState

	@model.methodwrap()
	def selectIdleProcess(self):
		self.currentp = ptypes.IdleProcRef
	
	@model.methodwrap()
	def SCHEDULENEXT(self):
		self.lck.Lock
		self.selectIdleProcess
		self.lck.Unlock
		return True

model_class = CURRENTPROCESS

